package com.googlecode.kipler.satisfiability.completion.rule.individual;

import java.util.Iterator;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.ConceptCategory;
import com.googlecode.kipler.container.dl.MarkedFormulaContainer;
import com.googlecode.kipler.satisfiability.blocking.abox.ABoxBlockingStrategy;
import com.googlecode.kipler.satisfiability.completion.branching.BetaBranchingPoint;
import com.googlecode.kipler.satisfiability.completion.rule.individual.uniformnotation.BetaConcept;
import com.googlecode.kipler.satisfiability.reasoner.BranchingException;
import com.googlecode.kipler.satisfiability.reasoner.Reasoner;
import com.googlecode.kipler.satisfiability.reasoner.ReasonerException;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.concept.Concept;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;

public class BetaConceptRule extends ABoxRule {

	private boolean applied;

	private Reasoner reasoner;

	private ABox aBox;

	private ABoxBlockingStrategy blocking;

	private ConceptCategory category;

	private BetaConcept beta;

	private String ruleName;

	private boolean marking;

	public BetaConceptRule(Reasoner reasoner, ABoxBlockingStrategy blocking,
			ConceptCategory category, BetaConcept beta, boolean marking,
			String ruleName) {
		setBlocking(blocking);
		this.reasoner = reasoner;
		this.category = category;
		this.beta = beta;
		this.ruleName = ruleName;
		this.marking = marking;
	}

	public ABoxBlockingStrategy getBlocking() {
		return blocking;
	}

	public void setBlocking(ABoxBlockingStrategy blocking) {
		this.blocking = blocking;
	}

	public boolean isApplied() {
		return applied;
	}

	@Override
	public void apply() throws ReasonerException {
		applied = false;
		aBox = getWorld().getABox();
		if (!getBlocking().isIndirectlyBlocked(aBox, getIndividual().getName())) {
			for (Iterator<Concept> i = getIndividual()
					.conceptIterator(category); i.hasNext();) {
				Concept concept = i.next();
				beta.setBeta(concept);
				if (beta.isValid()) {
					boolean toBeApplied = false;
					if (marking) {
						MarkedFormulaContainer wcsData = (MarkedFormulaContainer) getWcs()
								.getData();
						ConceptAssertion ca = new ConceptAssertion(concept,
								getIndividual().getName());
						toBeApplied = !wcsData.getMarkedFormulas().contains(ca);
					} else {
						toBeApplied = !getIndividual()
								.contains(beta.getBeta1())
								&& !getIndividual().contains(beta.getBeta2());
					}
					if (toBeApplied) {
						branchForConcepts(beta);
						applied = true;
						throw new BranchingException();
					}
				}
			}
		}
	}

	private void branchForConcepts(BetaConcept beta)
			throws UnsatisfiableException {
		ConceptAssertion assert1 = new ConceptAssertion(beta.getBeta1(),
				getIndividual().getName());
		ConceptAssertion assert2 = new ConceptAssertion(beta.getBeta2(),
				getIndividual().getName());
		BetaBranchingPoint bp = new BetaBranchingPoint(marking);
		bp.setWcs(getWcs());
		bp.setWorld(getWorld());
		bp.addFormula(assert1);
		bp.addFormula(assert2);
		bp.setBranchCause(new ConceptAssertion(beta.getBeta(), getIndividual()
				.getName()));
		reasoner.addBranch(bp);
		getWcs().getData().getLogger().info(
				"WCS " + getWcs().getId() + " " + ruleName + ": Branching for "
						+ assert1 + " and " + assert2);

	}

}
